es:ES, i:Id, P:({e:E| loc(e) = i }{e2:E| loc(e2) = i }Prop).
e1@i. e2e1.(e:E. (e1 <loc e)  e  e2   P(e,e2))  P(e1,e2)  e1@i. e2e1.P(e1,e2) 

latex

Definitions

e'e.P(e'), e@i. P(e), 1of(t), ES, Prop, x. t(x), P  Q, (e <loc e'), {T}, P  Q, P & Q, x(s1,s2), e  e' , P  Q, A, False, P  Q, b, E, Id, loc(e), x:A. B(x), t  T, , AB, ||as||, [e, e'], ij, (x  l), pred(e), S  T, Top

Lemmas

es-interval-non-zero, es-le-pred, top wf, es-interval wf2, es-pred wf, length-append, es-interval-partition, nil member, l member wf, es-interval wf, length zero, non neg length, es-le-self, member-es-interval, length wf1, le wf, nat wf, nat properties, ge wf, es-loc wf, Id wf, es-E wf, es-locl-iff, implies functionality wrt iff, all functionality wrt iff, es-loc-pred, es-le-loc, subtype rel self, es-le wf, es-locl wf, alle-at wf, alle-ge wf, event system wf